-
Notifications
You must be signed in to change notification settings - Fork 12.9k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Handle cycles in overlap with negative impls #109673
Handle cycles in overlap with negative impls #109673
Conversation
This comment has been minimized.
This comment has been minimized.
8262cf6
to
9443847
Compare
trait_pred, | ||
)) | ||
.expect("Overflow should be caught earlier in standard query mode") | ||
.must_apply_modulo_regions() |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why use this over predicate_may_hold
? Don't we want to treat treat ambiguity as "yes" instead of "no" for coherence purposes?
Sorry if this question is misunderstanding what this PR is trying to do.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The idea if I got everything correct is that we want to check that there's not a negative impl that applies. This is why I wanted to check for a must. But this is one of the things that I have doubts if using must_apply_module_regions
is correct here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should be may apply modulo regions, not must apply.
| ^^^^^^^^^^^^^^^^^^^^ | ||
| | | ||
| first implementation here | ||
| conflicting implementation |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ideally we'd find the impl that satisfies !MyTrait
and highlight it -- can we do that with SelectionContext::select
? This could be a follow-up I guess..
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, diagnostics are not really handled in the PR yet. Is one of the things that are still not complete.
compiler/rustc_trait_selection/src/traits/specialize/specialization_graph.rs
Outdated
Show resolved
Hide resolved
compiler/rustc_trait_selection/src/traits/specialize/specialization_graph.rs
Outdated
Show resolved
Hide resolved
☔ The latest upstream changes (presumably #108080) made this pull request unmergeable. Please resolve the merge conflicts. |
9443847
to
ba78cb9
Compare
ba78cb9
to
45ac61a
Compare
@@ -226,6 +226,22 @@ fn overlap_check_considering_specialization<'tcx>( | |||
return Ok(OverlapResult::SpecializeAll(replace_children)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Block: early returns
@@ -226,6 +226,22 @@ fn overlap_check_considering_specialization<'tcx>( | |||
return Ok(OverlapResult::SpecializeAll(replace_children)); | |||
} | |||
|
|||
if overlap_mode.use_negative_impl() |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
remove this if, but before you do, let's try to figure out why the src/test/ui/traits/negative-impls/pin-unsound-issue-66544-derefmut.rs
test gets an error (assuming it does...)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
probably because we didn't remove the old coherence logic
@@ -120,6 +120,48 @@ pub fn overlapping_impls( | |||
Some(overlap(selcx, skip_leak_check, impl1_def_id, impl2_def_id, overlap_mode).unwrap()) | |||
} | |||
|
|||
/// Given an impl_def_id that "positively" implement a trait, check if the "negative" holds. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
s/implement/implements/
@@ -120,6 +120,48 @@ pub fn overlapping_impls( | |||
Some(overlap(selcx, skip_leak_check, impl1_def_id, impl2_def_id, overlap_mode).unwrap()) | |||
} | |||
|
|||
/// Given an impl_def_id that "positively" implement a trait, check if the "negative" holds. | |||
pub fn negative_impl_holds(tcx: TyCtxt<'_>, impl_def_id: DefId, overlap_mode: OverlapMode) -> bool { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
s/negative_impl_holds/negative_impl_may_hold/
trait_pred, | ||
)) | ||
.expect("Overflow should be caught earlier in standard query mode") | ||
.must_apply_modulo_regions() |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should be may apply modulo regions, not must apply.
))); | ||
|
||
// Ideally we would use param_env(impl_def_id) but that's unsound today. | ||
let param_env = ty::ParamEnv::empty(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
To do this properly, what we ought to do is get the parameter environment and then apply the infer_substs
above. The idea is that for some impl...
impl<A..Z> SomeTrait<T1..Tn> for T0
where WC
we want to test if...
- there exists types
A..Z
such that... - assuming
WC
is true (ie., with the param env in scope)... T0: !SomeTrait<T1..Tn>
this would be an error, because that means that for at least some instance of this positive impl, there exists a negative impl.
Problem is: applying infer_substs
to param-env will mean that we have inference variables in the environment, and I think our code doesn't like that.
It should be sound to not assume WC is true, because proving A => X
is harder than proving X
on its own, but I'm worried we may be overly conservative.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
inference variables in the param env generally cause issues, especially in the old solver. Don't remember exactly what breaks but iirc @BoxyUwU encountered a bunch of issues recently when she tried it.
I think a bigger issue is that the way candidate_should_be_dropped_in_favor_of
handles param env candidates is incomplete. This means that coherence in the old solver with trait goals in the param env is unsound because inference may incorrectly cause another nested goal to fail, resulting in an incorrect error. My current approach for the new solver is to disable this behavior if we're in coherence: #109724
@spastorino any updates on this? |
@rustbot modify labels -S-waiting-on-review +S-waiting-on-author |
☔ The latest upstream changes (presumably #113591) made this pull request unmergeable. Please resolve the merge conflicts. |
This can be closed for now. |
Fixes #102678
r? @nikomatsakis
Opened this as a way to start reviewing it.
At the very least we have the following pending things:
I'd need to check a bit better to, to see if there's more to cover.